Left Termination proof of /tmp/tmpEPmiCw/ackermann-ioi.pl

Left Termination of the query pattern ackermann_in_3(g, a, g) w.r.t. the given Prolog program could not be shown:

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

Clauses:

ackermann(0, N, s(N)).
ackermann(s(M), 0, Val) :- ackermann(M, s(0), Val).
ackermann(s(M), s(N), Val) :- ','(ackermann(s(M), N, Val1), ackermann(M, Val1, Val)).

Queries:

ackermann(g,a,g).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
ackermann_in: (b,f,b) (f,b,b) (b,f,f) (f,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(0, N, s(N)) → ackermann_out_agg(0, N, s(N))
ackermann_in_agg(s(M), 0, Val) → U1_agg(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(s(M), s(N), Val) → U2_agg(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(0, N, s(N)) → ackermann_out_aga(0, N, s(N))
ackermann_in_aga(s(M), 0, Val) → U1_aga(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(s(M), s(N), Val) → U2_aga(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_aga(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_aga(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_aga(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s(M), s(N), Val)
U1_aga(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_aga(s(M), 0, Val)
U1_gaa(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_agg(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_agg(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_agg(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_agg(s(M), s(N), Val)
U1_agg(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_agg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

  ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(0, N, s(N)) → ackermann_out_agg(0, N, s(N))
ackermann_in_agg(s(M), 0, Val) → U1_agg(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(s(M), s(N), Val) → U2_agg(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(0, N, s(N)) → ackermann_out_aga(0, N, s(N))
ackermann_in_aga(s(M), 0, Val) → U1_aga(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(s(M), s(N), Val) → U2_aga(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_aga(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_aga(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_aga(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s(M), s(N), Val)
U1_aga(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_aga(s(M), 0, Val)
U1_gaa(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_agg(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_agg(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_agg(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_agg(s(M), s(N), Val)
U1_agg(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_agg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

ACKERMANN_IN_GAG(s(M), 0, Val) → U1_GAG(M, Val, ackermann_in_agg(M, s(0), Val))
ACKERMANN_IN_GAG(s(M), 0, Val) → ACKERMANN_IN_AGG(M, s(0), Val)
ACKERMANN_IN_AGG(s(M), 0, Val) → U1_AGG(M, Val, ackermann_in_agg(M, s(0), Val))
ACKERMANN_IN_AGG(s(M), 0, Val) → ACKERMANN_IN_AGG(M, s(0), Val)
ACKERMANN_IN_AGG(s(M), s(N), Val) → U2_AGG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_AGG(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_GAA(s(M), 0, Val) → U1_GAA(M, Val, ackermann_in_aga(M, s(0), Val))
ACKERMANN_IN_GAA(s(M), 0, Val) → ACKERMANN_IN_AGA(M, s(0), Val)
ACKERMANN_IN_AGA(s(M), 0, Val) → U1_AGA(M, Val, ackermann_in_aga(M, s(0), Val))
ACKERMANN_IN_AGA(s(M), 0, Val) → ACKERMANN_IN_AGA(M, s(0), Val)
ACKERMANN_IN_AGA(s(M), s(N), Val) → U2_AGA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_AGA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAA(M, N, Val, ackermann_in_aga(M, Val1, Val))
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGA(M, Val1, Val)
U2_AGA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_AGA(M, N, Val, ackermann_in_aga(M, Val1, Val))
U2_AGA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGA(M, Val1, Val)
U2_AGG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_AGG(M, N, Val, ackermann_in_agg(M, Val1, Val))
U2_AGG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGG(M, Val1, Val)
ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAG(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAG(M, N, Val, ackermann_in_agg(M, Val1, Val))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(0, N, s(N)) → ackermann_out_agg(0, N, s(N))
ackermann_in_agg(s(M), 0, Val) → U1_agg(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(s(M), s(N), Val) → U2_agg(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(0, N, s(N)) → ackermann_out_aga(0, N, s(N))
ackermann_in_aga(s(M), 0, Val) → U1_aga(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(s(M), s(N), Val) → U2_aga(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_aga(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_aga(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_aga(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s(M), s(N), Val)
U1_aga(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_aga(s(M), 0, Val)
U1_gaa(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_agg(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_agg(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_agg(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_agg(s(M), s(N), Val)
U1_agg(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_agg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

The argument filtering Pi contains the following mapping:
ackermann_in_gag(x1, x2, x3) = ackermann_in_gag(x1, x3)
0 = 0
s(x1) = s
ackermann_out_gag(x1, x2, x3) = ackermann_out_gag
U1_gag(x1, x2, x3) = U1_gag(x3)
U2_gag(x1, x2, x3, x4) = U2_gag(x3, x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa(x3)
ackermann_in_agg(x1, x2, x3) = ackermann_in_agg(x2, x3)
ackermann_out_agg(x1, x2, x3) = ackermann_out_agg(x1)
U1_agg(x1, x2, x3) = U1_agg(x3)
U2_agg(x1, x2, x3, x4) = U2_agg(x3, x4)
U1_gaa(x1, x2, x3) = U1_gaa(x3)
ackermann_in_aga(x1, x2, x3) = ackermann_in_aga(x2)
ackermann_out_aga(x1, x2, x3) = ackermann_out_aga(x1, x3)
U1_aga(x1, x2, x3) = U1_aga(x3)
U2_aga(x1, x2, x3, x4) = U2_aga(x4)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x4)
U3_aga(x1, x2, x3, x4) = U3_aga(x4)
U3_agg(x1, x2, x3, x4) = U3_agg(x4)
U3_gag(x1, x2, x3, x4) = U3_gag(x4)
U3_AGG(x1, x2, x3, x4) = U3_AGG(x4)
U1_AGA(x1, x2, x3) = U1_AGA(x3)
U3_GAG(x1, x2, x3, x4) = U3_GAG(x4)
U2_AGG(x1, x2, x3, x4) = U2_AGG(x3, x4)
U3_GAA(x1, x2, x3, x4) = U3_GAA(x4)
ACKERMANN_IN_GAG(x1, x2, x3) = ACKERMANN_IN_GAG(x1, x3)
ACKERMANN_IN_AGG(x1, x2, x3) = ACKERMANN_IN_AGG(x2, x3)
ACKERMANN_IN_GAA(x1, x2, x3) = ACKERMANN_IN_GAA(x1)
U2_AGA(x1, x2, x3, x4) = U2_AGA(x4)
U1_GAA(x1, x2, x3) = U1_GAA(x3)
U3_AGA(x1, x2, x3, x4) = U3_AGA(x4)
U1_GAG(x1, x2, x3) = U1_GAG(x3)
ACKERMANN_IN_AGA(x1, x2, x3) = ACKERMANN_IN_AGA(x2)
U1_AGG(x1, x2, x3) = U1_AGG(x3)
U2_GAG(x1, x2, x3, x4) = U2_GAG(x3, x4)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x4)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), 0, Val) → U1_GAG(M, Val, ackermann_in_agg(M, s(0), Val))
ACKERMANN_IN_GAG(s(M), 0, Val) → ACKERMANN_IN_AGG(M, s(0), Val)
ACKERMANN_IN_AGG(s(M), 0, Val) → U1_AGG(M, Val, ackermann_in_agg(M, s(0), Val))
ACKERMANN_IN_AGG(s(M), 0, Val) → ACKERMANN_IN_AGG(M, s(0), Val)
ACKERMANN_IN_AGG(s(M), s(N), Val) → U2_AGG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_AGG(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_GAA(s(M), 0, Val) → U1_GAA(M, Val, ackermann_in_aga(M, s(0), Val))
ACKERMANN_IN_GAA(s(M), 0, Val) → ACKERMANN_IN_AGA(M, s(0), Val)
ACKERMANN_IN_AGA(s(M), 0, Val) → U1_AGA(M, Val, ackermann_in_aga(M, s(0), Val))
ACKERMANN_IN_AGA(s(M), 0, Val) → ACKERMANN_IN_AGA(M, s(0), Val)
ACKERMANN_IN_AGA(s(M), s(N), Val) → U2_AGA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_AGA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAA(M, N, Val, ackermann_in_aga(M, Val1, Val))
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGA(M, Val1, Val)
U2_AGA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_AGA(M, N, Val, ackermann_in_aga(M, Val1, Val))
U2_AGA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGA(M, Val1, Val)
U2_AGG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_AGG(M, N, Val, ackermann_in_agg(M, Val1, Val))
U2_AGG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGG(M, Val1, Val)
ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAG(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAG(M, N, Val, ackermann_in_agg(M, Val1, Val))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(0, N, s(N)) → ackermann_out_agg(0, N, s(N))
ackermann_in_agg(s(M), 0, Val) → U1_agg(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(s(M), s(N), Val) → U2_agg(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(0, N, s(N)) → ackermann_out_aga(0, N, s(N))
ackermann_in_aga(s(M), 0, Val) → U1_aga(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(s(M), s(N), Val) → U2_aga(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_aga(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_aga(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_aga(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s(M), s(N), Val)
U1_aga(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_aga(s(M), 0, Val)
U1_gaa(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_agg(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_agg(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_agg(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_agg(s(M), s(N), Val)
U1_agg(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_agg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_AGA(s(M), s(N), Val) → U2_AGA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_AGA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_AGA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGA(M, Val1, Val)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGA(M, Val1, Val)
ACKERMANN_IN_AGA(s(M), 0, Val) → ACKERMANN_IN_AGA(M, s(0), Val)
ACKERMANN_IN_GAA(s(M), 0, Val) → ACKERMANN_IN_AGA(M, s(0), Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(0, N, s(N)) → ackermann_out_agg(0, N, s(N))
ackermann_in_agg(s(M), 0, Val) → U1_agg(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(s(M), s(N), Val) → U2_agg(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(0, N, s(N)) → ackermann_out_aga(0, N, s(N))
ackermann_in_aga(s(M), 0, Val) → U1_aga(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(s(M), s(N), Val) → U2_aga(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_aga(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_aga(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_aga(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s(M), s(N), Val)
U1_aga(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_aga(s(M), 0, Val)
U1_gaa(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_agg(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_agg(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_agg(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_agg(s(M), s(N), Val)
U1_agg(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_agg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

The argument filtering Pi contains the following mapping:
ackermann_in_gag(x1, x2, x3) = ackermann_in_gag(x1, x3)
0 = 0
s(x1) = s
ackermann_out_gag(x1, x2, x3) = ackermann_out_gag
U1_gag(x1, x2, x3) = U1_gag(x3)
U2_gag(x1, x2, x3, x4) = U2_gag(x3, x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa(x3)
ackermann_in_agg(x1, x2, x3) = ackermann_in_agg(x2, x3)
ackermann_out_agg(x1, x2, x3) = ackermann_out_agg(x1)
U1_agg(x1, x2, x3) = U1_agg(x3)
U2_agg(x1, x2, x3, x4) = U2_agg(x3, x4)
U1_gaa(x1, x2, x3) = U1_gaa(x3)
ackermann_in_aga(x1, x2, x3) = ackermann_in_aga(x2)
ackermann_out_aga(x1, x2, x3) = ackermann_out_aga(x1, x3)
U1_aga(x1, x2, x3) = U1_aga(x3)
U2_aga(x1, x2, x3, x4) = U2_aga(x4)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x4)
U3_aga(x1, x2, x3, x4) = U3_aga(x4)
U3_agg(x1, x2, x3, x4) = U3_agg(x4)
U3_gag(x1, x2, x3, x4) = U3_gag(x4)
ACKERMANN_IN_GAA(x1, x2, x3) = ACKERMANN_IN_GAA(x1)
U2_AGA(x1, x2, x3, x4) = U2_AGA(x4)
ACKERMANN_IN_AGA(x1, x2, x3) = ACKERMANN_IN_AGA(x2)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_AGA(s(M), s(N), Val) → U2_AGA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_AGA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_AGA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGA(M, Val1, Val)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGA(M, Val1, Val)
ACKERMANN_IN_AGA(s(M), 0, Val) → ACKERMANN_IN_AGA(M, s(0), Val)
ACKERMANN_IN_GAA(s(M), 0, Val) → ACKERMANN_IN_AGA(M, s(0), Val)

The TRS R consists of the following rules:

ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U1_gaa(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_aga(M, Val1, Val))
ackermann_in_aga(0, N, s(N)) → ackermann_out_aga(0, N, s(N))
ackermann_in_aga(s(M), s(N), Val) → U2_aga(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U3_gaa(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_aga(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_aga(M, N, Val, ackermann_in_aga(M, Val1, Val))
ackermann_in_aga(s(M), 0, Val) → U1_aga(M, Val, ackermann_in_aga(M, s(0), Val))
U3_aga(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s(M), s(N), Val)
U1_aga(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_aga(s(M), 0, Val)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa(x3)
U1_gaa(x1, x2, x3) = U1_gaa(x3)
ackermann_in_aga(x1, x2, x3) = ackermann_in_aga(x2)
ackermann_out_aga(x1, x2, x3) = ackermann_out_aga(x1, x3)
U1_aga(x1, x2, x3) = U1_aga(x3)
U2_aga(x1, x2, x3, x4) = U2_aga(x4)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x4)
U3_aga(x1, x2, x3, x4) = U3_aga(x4)
ACKERMANN_IN_GAA(x1, x2, x3) = ACKERMANN_IN_GAA(x1)
U2_AGA(x1, x2, x3, x4) = U2_AGA(x4)
ACKERMANN_IN_AGA(x1, x2, x3) = ACKERMANN_IN_AGA(x2)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_AGA(0) → ACKERMANN_IN_AGA(s)
U2_AGA(ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGA(Val1)
ACKERMANN_IN_GAA(s) → U2_GAA(ackermann_in_gaa(s))
ACKERMANN_IN_AGA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_AGA(s) → U2_AGA(ackermann_in_gaa(s))
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_AGA(s)
U2_GAA(ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGA(Val1)

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_gaa(ackermann_out_gaa(Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_aga(ackermann_out_gaa(Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)
U1_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

ACKERMANN_IN_AGA(0) → ACKERMANN_IN_AGA(s)

The remaining pairs can at least be oriented weakly.

U2_AGA(ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGA(Val1)
ACKERMANN_IN_GAA(s) → U2_GAA(ackermann_in_gaa(s))
ACKERMANN_IN_AGA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_AGA(s) → U2_AGA(ackermann_in_gaa(s))
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_AGA(s)
U2_GAA(ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGA(Val1)

Used ordering: Polynomial interpretation [25]:

POL(0) = 1
POL(ACKERMANN_IN_AGA(x₁)) = x₁
POL(ACKERMANN_IN_GAA(x₁)) = 0
POL(U1_aga(x₁)) = x₁
POL(U1_gaa(x₁)) = x₁
POL(U2_AGA(x₁)) = x₁
POL(U2_GAA(x₁)) = x₁
POL(U2_aga(x₁)) = 0
POL(U2_gaa(x₁)) = 0
POL(U3_aga(x₁)) = x₁
POL(U3_gaa(x₁)) = x₁
POL(ackermann_in_aga(x₁)) = 0
POL(ackermann_in_gaa(x₁)) = 0
POL(ackermann_out_aga(x₁, x₂)) = x₂
POL(ackermann_out_gaa(x₁)) = x₁
POL(s) = 0

The following usable rules [17] were oriented:

ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U3_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
U1_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)
ackermann_in_aga(N) → ackermann_out_aga(0, s)
U2_aga(ackermann_out_gaa(Val1)) → U3_aga(ackermann_in_aga(Val1))
U2_gaa(ackermann_out_gaa(Val1)) → U3_gaa(ackermann_in_aga(Val1))
U1_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ Narrowing

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U2_AGA(ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGA(Val1)
ACKERMANN_IN_GAA(s) → U2_GAA(ackermann_in_gaa(s))
ACKERMANN_IN_AGA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_AGA(s) → U2_AGA(ackermann_in_gaa(s))
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_AGA(s)
U2_GAA(ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGA(Val1)

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_gaa(ackermann_out_gaa(Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_aga(ackermann_out_gaa(Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)
U1_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule ACKERMANN_IN_GAA(s) → U2_GAA(ackermann_in_gaa(s)) at position [0] we obtained the following new rules:

ACKERMANN_IN_GAA(s) → U2_GAA(U2_gaa(ackermann_in_gaa(s)))
ACKERMANN_IN_GAA(s) → U2_GAA(U1_gaa(ackermann_in_aga(s)))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s) → U2_GAA(U2_gaa(ackermann_in_gaa(s)))
U2_AGA(ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGA(Val1)
ACKERMANN_IN_GAA(s) → U2_GAA(U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_AGA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_AGA(s) → U2_AGA(ackermann_in_gaa(s))
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_AGA(s)
U2_GAA(ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGA(Val1)

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_gaa(ackermann_out_gaa(Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_aga(ackermann_out_gaa(Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)
U1_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule ACKERMANN_IN_AGA(s) → U2_AGA(ackermann_in_gaa(s)) at position [0] we obtained the following new rules:

ACKERMANN_IN_AGA(s) → U2_AGA(U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_AGA(s) → U2_AGA(U2_gaa(ackermann_in_gaa(s)))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ ForwardInstantiation

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s) → U2_GAA(U2_gaa(ackermann_in_gaa(s)))
U2_AGA(ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGA(Val1)
ACKERMANN_IN_AGA(s) → U2_AGA(U2_gaa(ackermann_in_gaa(s)))
ACKERMANN_IN_GAA(s) → U2_GAA(U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_AGA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_AGA(s) → U2_AGA(U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_AGA(s)
U2_GAA(ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGA(Val1)

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_gaa(ackermann_out_gaa(Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_aga(ackermann_out_gaa(Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)
U1_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
By forward instantiating [14] the rule U2_AGA(ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGA(Val1) we obtained the following new rules:

U2_AGA(ackermann_out_gaa(s)) → ACKERMANN_IN_AGA(s)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U2_AGA(ackermann_out_gaa(s)) → ACKERMANN_IN_AGA(s)
ACKERMANN_IN_GAA(s) → U2_GAA(U2_gaa(ackermann_in_gaa(s)))
ACKERMANN_IN_GAA(s) → U2_GAA(U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_AGA(s) → U2_AGA(U2_gaa(ackermann_in_gaa(s)))
ACKERMANN_IN_AGA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_AGA(s) → U2_AGA(U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_AGA(s)
U2_GAA(ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGA(Val1)

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_gaa(ackermann_out_gaa(Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_aga(ackermann_out_gaa(Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)
U1_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
By forward instantiating [14] the rule U2_GAA(ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGA(Val1) we obtained the following new rules:

U2_GAA(ackermann_out_gaa(s)) → ACKERMANN_IN_AGA(s)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

                                          ↳ QDP

                                            ↳ NonTerminationProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U2_AGA(ackermann_out_gaa(s)) → ACKERMANN_IN_AGA(s)
ACKERMANN_IN_GAA(s) → U2_GAA(U2_gaa(ackermann_in_gaa(s)))
ACKERMANN_IN_AGA(s) → U2_AGA(U2_gaa(ackermann_in_gaa(s)))
ACKERMANN_IN_GAA(s) → U2_GAA(U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_AGA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_AGA(s) → U2_AGA(U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_AGA(s)
U2_GAA(ackermann_out_gaa(s)) → ACKERMANN_IN_AGA(s)

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_gaa(ackermann_out_gaa(Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_aga(ackermann_out_gaa(Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)
U1_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

U2_AGA(ackermann_out_gaa(s)) → ACKERMANN_IN_AGA(s)
ACKERMANN_IN_GAA(s) → U2_GAA(U2_gaa(ackermann_in_gaa(s)))
ACKERMANN_IN_AGA(s) → U2_AGA(U2_gaa(ackermann_in_gaa(s)))
ACKERMANN_IN_GAA(s) → U2_GAA(U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_AGA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_AGA(s) → U2_AGA(U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_AGA(s)
U2_GAA(ackermann_out_gaa(s)) → ACKERMANN_IN_AGA(s)

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_gaa(ackermann_out_gaa(Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_aga(ackermann_out_gaa(Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)
U1_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)

s = ACKERMANN_IN_GAA(s) evaluates to t =ACKERMANN_IN_GAA(s)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from ACKERMANN_IN_GAA(s) to ACKERMANN_IN_GAA(s).

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_AGG(s(M), s(N), Val) → U2_AGG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_AGG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGG(M, Val1, Val)
ACKERMANN_IN_AGG(s(M), 0, Val) → ACKERMANN_IN_AGG(M, s(0), Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(0, N, s(N)) → ackermann_out_agg(0, N, s(N))
ackermann_in_agg(s(M), 0, Val) → U1_agg(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(s(M), s(N), Val) → U2_agg(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(0, N, s(N)) → ackermann_out_aga(0, N, s(N))
ackermann_in_aga(s(M), 0, Val) → U1_aga(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(s(M), s(N), Val) → U2_aga(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_aga(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_aga(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_aga(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s(M), s(N), Val)
U1_aga(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_aga(s(M), 0, Val)
U1_gaa(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_agg(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_agg(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_agg(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_agg(s(M), s(N), Val)
U1_agg(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_agg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_AGG(s(M), s(N), Val) → U2_AGG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_AGG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGG(M, Val1, Val)
ACKERMANN_IN_AGG(s(M), 0, Val) → ACKERMANN_IN_AGG(M, s(0), Val)

The TRS R consists of the following rules:

ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U1_gaa(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_aga(M, Val1, Val))
ackermann_in_aga(0, N, s(N)) → ackermann_out_aga(0, N, s(N))
ackermann_in_aga(s(M), s(N), Val) → U2_aga(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U3_gaa(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_aga(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_aga(M, N, Val, ackermann_in_aga(M, Val1, Val))
ackermann_in_aga(s(M), 0, Val) → U1_aga(M, Val, ackermann_in_aga(M, s(0), Val))
U3_aga(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s(M), s(N), Val)
U1_aga(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_aga(s(M), 0, Val)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa(x3)
U1_gaa(x1, x2, x3) = U1_gaa(x3)
ackermann_in_aga(x1, x2, x3) = ackermann_in_aga(x2)
ackermann_out_aga(x1, x2, x3) = ackermann_out_aga(x1, x3)
U1_aga(x1, x2, x3) = U1_aga(x3)
U2_aga(x1, x2, x3, x4) = U2_aga(x4)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x4)
U3_aga(x1, x2, x3, x4) = U3_aga(x4)
U2_AGG(x1, x2, x3, x4) = U2_AGG(x3, x4)
ACKERMANN_IN_AGG(x1, x2, x3) = ACKERMANN_IN_AGG(x2, x3)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_AGG(0, Val) → ACKERMANN_IN_AGG(s, Val)
U2_AGG(Val, ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGG(Val1, Val)
ACKERMANN_IN_AGG(s, Val) → U2_AGG(Val, ackermann_in_gaa(s))

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_gaa(ackermann_out_gaa(Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_aga(ackermann_out_gaa(Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)
U1_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

ACKERMANN_IN_AGG(0, Val) → ACKERMANN_IN_AGG(s, Val)

The remaining pairs can at least be oriented weakly.

U2_AGG(Val, ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGG(Val1, Val)
ACKERMANN_IN_AGG(s, Val) → U2_AGG(Val, ackermann_in_gaa(s))

Used ordering: Polynomial interpretation [25]:

POL(0) = 1
POL(ACKERMANN_IN_AGG(x₁, x₂)) = x₁
POL(U1_aga(x₁)) = x₁
POL(U1_gaa(x₁)) = x₁
POL(U2_AGG(x₁, x₂)) = x₂
POL(U2_aga(x₁)) = x₁
POL(U2_gaa(x₁)) = x₁
POL(U3_aga(x₁)) = x₁
POL(U3_gaa(x₁)) = x₁
POL(ackermann_in_aga(x₁)) = 0
POL(ackermann_in_gaa(x₁)) = 0
POL(ackermann_out_aga(x₁, x₂)) = x₂
POL(ackermann_out_gaa(x₁)) = x₁
POL(s) = 0

The following usable rules [17] were oriented:

U1_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U1_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U3_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)
ackermann_in_aga(N) → ackermann_out_aga(0, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U2_aga(ackermann_out_gaa(Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
U2_gaa(ackermann_out_gaa(Val1)) → U3_gaa(ackermann_in_aga(Val1))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ Narrowing

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U2_AGG(Val, ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGG(Val1, Val)
ACKERMANN_IN_AGG(s, Val) → U2_AGG(Val, ackermann_in_gaa(s))

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_gaa(ackermann_out_gaa(Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_aga(ackermann_out_gaa(Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)
U1_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule ACKERMANN_IN_AGG(s, Val) → U2_AGG(Val, ackermann_in_gaa(s)) at position [1] we obtained the following new rules:

ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U2_gaa(ackermann_in_gaa(s)))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ ForwardInstantiation

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U1_gaa(ackermann_in_aga(s)))
U2_AGG(Val, ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGG(Val1, Val)
ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U2_gaa(ackermann_in_gaa(s)))

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_gaa(ackermann_out_gaa(Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_aga(ackermann_out_gaa(Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)
U1_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
By forward instantiating [14] the rule U2_AGG(Val, ackermann_out_gaa(Val1)) → ACKERMANN_IN_AGG(Val1, Val) we obtained the following new rules:

U2_AGG(x0, ackermann_out_gaa(s)) → ACKERMANN_IN_AGG(s, x0)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ ForwardInstantiation

                                  ↳ QDP

                                    ↳ NonTerminationProof

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U1_gaa(ackermann_in_aga(s)))
U2_AGG(x0, ackermann_out_gaa(s)) → ACKERMANN_IN_AGG(s, x0)
ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U2_gaa(ackermann_in_gaa(s)))

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_gaa(ackermann_out_gaa(Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_aga(ackermann_out_gaa(Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)
U1_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U1_gaa(ackermann_in_aga(s)))
U2_AGG(x0, ackermann_out_gaa(s)) → ACKERMANN_IN_AGG(s, x0)
ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U2_gaa(ackermann_in_gaa(s)))

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_gaa(ackermann_out_gaa(Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val)
U2_aga(ackermann_out_gaa(Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)
U1_aga(ackermann_out_aga(M, Val)) → ackermann_out_aga(s, Val)

s = U2_AGG(x0, U1_gaa(ackermann_in_aga(N))) evaluates to t =U2_AGG(x0, U1_gaa(ackermann_in_aga(s)))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [N / s]
Semiunifier: [ ]

Rewriting sequence

U2_AGG(x0, U1_gaa(ackermann_in_aga(N))) → U2_AGG(x0, U1_gaa(ackermann_out_aga(0, s)))
with rule ackermann_in_aga(N') → ackermann_out_aga(0, s) at position [1,0] and matcher [N' / N]

U2_AGG(x0, U1_gaa(ackermann_out_aga(0, s))) → U2_AGG(x0, ackermann_out_gaa(s))
with rule U1_gaa(ackermann_out_aga(M, Val)) → ackermann_out_gaa(Val) at position [1] and matcher [M / 0, Val / s]

U2_AGG(x0, ackermann_out_gaa(s)) → ACKERMANN_IN_AGG(s, x0)
with rule U2_AGG(x0', ackermann_out_gaa(s)) → ACKERMANN_IN_AGG(s, x0') at position [] and matcher [x0' / x0]

ACKERMANN_IN_AGG(s, x0) → U2_AGG(x0, U1_gaa(ackermann_in_aga(s)))
with rule ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U1_gaa(ackermann_in_aga(s)))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
ackermann_in: (b,f,b) (f,b,b) (b,f,f) (f,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(0, N, s(N)) → ackermann_out_agg(0, N, s(N))
ackermann_in_agg(s(M), 0, Val) → U1_agg(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(s(M), s(N), Val) → U2_agg(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(0, N, s(N)) → ackermann_out_aga(0, N, s(N))
ackermann_in_aga(s(M), 0, Val) → U1_aga(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(s(M), s(N), Val) → U2_aga(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_aga(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_aga(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_aga(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s(M), s(N), Val)
U1_aga(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_aga(s(M), 0, Val)
U1_gaa(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_agg(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_agg(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_agg(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_agg(s(M), s(N), Val)
U1_agg(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_agg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(0, N, s(N)) → ackermann_out_agg(0, N, s(N))
ackermann_in_agg(s(M), 0, Val) → U1_agg(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(s(M), s(N), Val) → U2_agg(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(0, N, s(N)) → ackermann_out_aga(0, N, s(N))
ackermann_in_aga(s(M), 0, Val) → U1_aga(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(s(M), s(N), Val) → U2_aga(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_aga(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_aga(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_aga(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s(M), s(N), Val)
U1_aga(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_aga(s(M), 0, Val)
U1_gaa(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_agg(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_agg(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_agg(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_agg(s(M), s(N), Val)
U1_agg(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_agg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

ACKERMANN_IN_GAG(s(M), 0, Val) → U1_GAG(M, Val, ackermann_in_agg(M, s(0), Val))
ACKERMANN_IN_GAG(s(M), 0, Val) → ACKERMANN_IN_AGG(M, s(0), Val)
ACKERMANN_IN_AGG(s(M), 0, Val) → U1_AGG(M, Val, ackermann_in_agg(M, s(0), Val))
ACKERMANN_IN_AGG(s(M), 0, Val) → ACKERMANN_IN_AGG(M, s(0), Val)
ACKERMANN_IN_AGG(s(M), s(N), Val) → U2_AGG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_AGG(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_GAA(s(M), 0, Val) → U1_GAA(M, Val, ackermann_in_aga(M, s(0), Val))
ACKERMANN_IN_GAA(s(M), 0, Val) → ACKERMANN_IN_AGA(M, s(0), Val)
ACKERMANN_IN_AGA(s(M), 0, Val) → U1_AGA(M, Val, ackermann_in_aga(M, s(0), Val))
ACKERMANN_IN_AGA(s(M), 0, Val) → ACKERMANN_IN_AGA(M, s(0), Val)
ACKERMANN_IN_AGA(s(M), s(N), Val) → U2_AGA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_AGA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAA(M, N, Val, ackermann_in_aga(M, Val1, Val))
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGA(M, Val1, Val)
U2_AGA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_AGA(M, N, Val, ackermann_in_aga(M, Val1, Val))
U2_AGA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGA(M, Val1, Val)
U2_AGG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_AGG(M, N, Val, ackermann_in_agg(M, Val1, Val))
U2_AGG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGG(M, Val1, Val)
ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAG(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAG(M, N, Val, ackermann_in_agg(M, Val1, Val))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(0, N, s(N)) → ackermann_out_agg(0, N, s(N))
ackermann_in_agg(s(M), 0, Val) → U1_agg(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(s(M), s(N), Val) → U2_agg(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(0, N, s(N)) → ackermann_out_aga(0, N, s(N))
ackermann_in_aga(s(M), 0, Val) → U1_aga(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(s(M), s(N), Val) → U2_aga(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_aga(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_aga(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_aga(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s(M), s(N), Val)
U1_aga(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_aga(s(M), 0, Val)
U1_gaa(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_agg(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_agg(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_agg(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_agg(s(M), s(N), Val)
U1_agg(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_agg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

The argument filtering Pi contains the following mapping:
ackermann_in_gag(x1, x2, x3) = ackermann_in_gag(x1, x3)
0 = 0
s(x1) = s
ackermann_out_gag(x1, x2, x3) = ackermann_out_gag(x1, x3)
U1_gag(x1, x2, x3) = U1_gag(x2, x3)
U2_gag(x1, x2, x3, x4) = U2_gag(x3, x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa(x1, x3)
ackermann_in_agg(x1, x2, x3) = ackermann_in_agg(x2, x3)
ackermann_out_agg(x1, x2, x3) = ackermann_out_agg(x1, x2, x3)
U1_agg(x1, x2, x3) = U1_agg(x2, x3)
U2_agg(x1, x2, x3, x4) = U2_agg(x3, x4)
U1_gaa(x1, x2, x3) = U1_gaa(x3)
ackermann_in_aga(x1, x2, x3) = ackermann_in_aga(x2)
ackermann_out_aga(x1, x2, x3) = ackermann_out_aga(x1, x2, x3)
U1_aga(x1, x2, x3) = U1_aga(x3)
U2_aga(x1, x2, x3, x4) = U2_aga(x4)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x4)
U3_aga(x1, x2, x3, x4) = U3_aga(x4)
U3_agg(x1, x2, x3, x4) = U3_agg(x3, x4)
U3_gag(x1, x2, x3, x4) = U3_gag(x3, x4)
U3_AGG(x1, x2, x3, x4) = U3_AGG(x3, x4)
U1_AGA(x1, x2, x3) = U1_AGA(x3)
U3_GAG(x1, x2, x3, x4) = U3_GAG(x3, x4)
U2_AGG(x1, x2, x3, x4) = U2_AGG(x3, x4)
U3_GAA(x1, x2, x3, x4) = U3_GAA(x4)
ACKERMANN_IN_GAG(x1, x2, x3) = ACKERMANN_IN_GAG(x1, x3)
ACKERMANN_IN_AGG(x1, x2, x3) = ACKERMANN_IN_AGG(x2, x3)
ACKERMANN_IN_GAA(x1, x2, x3) = ACKERMANN_IN_GAA(x1)
U2_AGA(x1, x2, x3, x4) = U2_AGA(x4)
U1_GAA(x1, x2, x3) = U1_GAA(x3)
U3_AGA(x1, x2, x3, x4) = U3_AGA(x4)
U1_GAG(x1, x2, x3) = U1_GAG(x2, x3)
ACKERMANN_IN_AGA(x1, x2, x3) = ACKERMANN_IN_AGA(x2)
U1_AGG(x1, x2, x3) = U1_AGG(x2, x3)
U2_GAG(x1, x2, x3, x4) = U2_GAG(x3, x4)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x4)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), 0, Val) → U1_GAG(M, Val, ackermann_in_agg(M, s(0), Val))
ACKERMANN_IN_GAG(s(M), 0, Val) → ACKERMANN_IN_AGG(M, s(0), Val)
ACKERMANN_IN_AGG(s(M), 0, Val) → U1_AGG(M, Val, ackermann_in_agg(M, s(0), Val))
ACKERMANN_IN_AGG(s(M), 0, Val) → ACKERMANN_IN_AGG(M, s(0), Val)
ACKERMANN_IN_AGG(s(M), s(N), Val) → U2_AGG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_AGG(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_GAA(s(M), 0, Val) → U1_GAA(M, Val, ackermann_in_aga(M, s(0), Val))
ACKERMANN_IN_GAA(s(M), 0, Val) → ACKERMANN_IN_AGA(M, s(0), Val)
ACKERMANN_IN_AGA(s(M), 0, Val) → U1_AGA(M, Val, ackermann_in_aga(M, s(0), Val))
ACKERMANN_IN_AGA(s(M), 0, Val) → ACKERMANN_IN_AGA(M, s(0), Val)
ACKERMANN_IN_AGA(s(M), s(N), Val) → U2_AGA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_AGA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAA(M, N, Val, ackermann_in_aga(M, Val1, Val))
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGA(M, Val1, Val)
U2_AGA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_AGA(M, N, Val, ackermann_in_aga(M, Val1, Val))
U2_AGA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGA(M, Val1, Val)
U2_AGG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_AGG(M, N, Val, ackermann_in_agg(M, Val1, Val))
U2_AGG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGG(M, Val1, Val)
ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAG(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAG(M, N, Val, ackermann_in_agg(M, Val1, Val))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(0, N, s(N)) → ackermann_out_agg(0, N, s(N))
ackermann_in_agg(s(M), 0, Val) → U1_agg(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(s(M), s(N), Val) → U2_agg(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(0, N, s(N)) → ackermann_out_aga(0, N, s(N))
ackermann_in_aga(s(M), 0, Val) → U1_aga(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(s(M), s(N), Val) → U2_aga(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_aga(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_aga(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_aga(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s(M), s(N), Val)
U1_aga(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_aga(s(M), 0, Val)
U1_gaa(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_agg(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_agg(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_agg(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_agg(s(M), s(N), Val)
U1_agg(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_agg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

The argument filtering Pi contains the following mapping:
ackermann_in_gag(x1, x2, x3) = ackermann_in_gag(x1, x3)
0 = 0
s(x1) = s
ackermann_out_gag(x1, x2, x3) = ackermann_out_gag(x1, x3)
U1_gag(x1, x2, x3) = U1_gag(x2, x3)
U2_gag(x1, x2, x3, x4) = U2_gag(x3, x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa(x1, x3)
ackermann_in_agg(x1, x2, x3) = ackermann_in_agg(x2, x3)
ackermann_out_agg(x1, x2, x3) = ackermann_out_agg(x1, x2, x3)
U1_agg(x1, x2, x3) = U1_agg(x2, x3)
U2_agg(x1, x2, x3, x4) = U2_agg(x3, x4)
U1_gaa(x1, x2, x3) = U1_gaa(x3)
ackermann_in_aga(x1, x2, x3) = ackermann_in_aga(x2)
ackermann_out_aga(x1, x2, x3) = ackermann_out_aga(x1, x2, x3)
U1_aga(x1, x2, x3) = U1_aga(x3)
U2_aga(x1, x2, x3, x4) = U2_aga(x4)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x4)
U3_aga(x1, x2, x3, x4) = U3_aga(x4)
U3_agg(x1, x2, x3, x4) = U3_agg(x3, x4)
U3_gag(x1, x2, x3, x4) = U3_gag(x3, x4)
U3_AGG(x1, x2, x3, x4) = U3_AGG(x3, x4)
U1_AGA(x1, x2, x3) = U1_AGA(x3)
U3_GAG(x1, x2, x3, x4) = U3_GAG(x3, x4)
U2_AGG(x1, x2, x3, x4) = U2_AGG(x3, x4)
U3_GAA(x1, x2, x3, x4) = U3_GAA(x4)
ACKERMANN_IN_GAG(x1, x2, x3) = ACKERMANN_IN_GAG(x1, x3)
ACKERMANN_IN_AGG(x1, x2, x3) = ACKERMANN_IN_AGG(x2, x3)
ACKERMANN_IN_GAA(x1, x2, x3) = ACKERMANN_IN_GAA(x1)
U2_AGA(x1, x2, x3, x4) = U2_AGA(x4)
U1_GAA(x1, x2, x3) = U1_GAA(x3)
U3_AGA(x1, x2, x3, x4) = U3_AGA(x4)
U1_GAG(x1, x2, x3) = U1_GAG(x2, x3)
ACKERMANN_IN_AGA(x1, x2, x3) = ACKERMANN_IN_AGA(x2)
U1_AGG(x1, x2, x3) = U1_AGG(x2, x3)
U2_GAG(x1, x2, x3, x4) = U2_GAG(x3, x4)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x4)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 2 SCCs with 13 less nodes.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_AGA(s(M), s(N), Val) → U2_AGA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_AGA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_AGA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGA(M, Val1, Val)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGA(M, Val1, Val)
ACKERMANN_IN_AGA(s(M), 0, Val) → ACKERMANN_IN_AGA(M, s(0), Val)
ACKERMANN_IN_GAA(s(M), 0, Val) → ACKERMANN_IN_AGA(M, s(0), Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(0, N, s(N)) → ackermann_out_agg(0, N, s(N))
ackermann_in_agg(s(M), 0, Val) → U1_agg(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(s(M), s(N), Val) → U2_agg(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(0, N, s(N)) → ackermann_out_aga(0, N, s(N))
ackermann_in_aga(s(M), 0, Val) → U1_aga(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(s(M), s(N), Val) → U2_aga(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_aga(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_aga(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_aga(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s(M), s(N), Val)
U1_aga(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_aga(s(M), 0, Val)
U1_gaa(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_agg(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_agg(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_agg(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_agg(s(M), s(N), Val)
U1_agg(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_agg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

The argument filtering Pi contains the following mapping:
ackermann_in_gag(x1, x2, x3) = ackermann_in_gag(x1, x3)
0 = 0
s(x1) = s
ackermann_out_gag(x1, x2, x3) = ackermann_out_gag(x1, x3)
U1_gag(x1, x2, x3) = U1_gag(x2, x3)
U2_gag(x1, x2, x3, x4) = U2_gag(x3, x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa(x1, x3)
ackermann_in_agg(x1, x2, x3) = ackermann_in_agg(x2, x3)
ackermann_out_agg(x1, x2, x3) = ackermann_out_agg(x1, x2, x3)
U1_agg(x1, x2, x3) = U1_agg(x2, x3)
U2_agg(x1, x2, x3, x4) = U2_agg(x3, x4)
U1_gaa(x1, x2, x3) = U1_gaa(x3)
ackermann_in_aga(x1, x2, x3) = ackermann_in_aga(x2)
ackermann_out_aga(x1, x2, x3) = ackermann_out_aga(x1, x2, x3)
U1_aga(x1, x2, x3) = U1_aga(x3)
U2_aga(x1, x2, x3, x4) = U2_aga(x4)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x4)
U3_aga(x1, x2, x3, x4) = U3_aga(x4)
U3_agg(x1, x2, x3, x4) = U3_agg(x3, x4)
U3_gag(x1, x2, x3, x4) = U3_gag(x3, x4)
ACKERMANN_IN_GAA(x1, x2, x3) = ACKERMANN_IN_GAA(x1)
U2_AGA(x1, x2, x3, x4) = U2_AGA(x4)
ACKERMANN_IN_AGA(x1, x2, x3) = ACKERMANN_IN_AGA(x2)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_AGA(s(M), s(N), Val) → U2_AGA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_AGA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_AGA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGA(M, Val1, Val)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGA(M, Val1, Val)
ACKERMANN_IN_AGA(s(M), 0, Val) → ACKERMANN_IN_AGA(M, s(0), Val)
ACKERMANN_IN_GAA(s(M), 0, Val) → ACKERMANN_IN_AGA(M, s(0), Val)

The TRS R consists of the following rules:

ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U1_gaa(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_aga(M, Val1, Val))
ackermann_in_aga(0, N, s(N)) → ackermann_out_aga(0, N, s(N))
ackermann_in_aga(s(M), s(N), Val) → U2_aga(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U3_gaa(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_aga(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_aga(M, N, Val, ackermann_in_aga(M, Val1, Val))
ackermann_in_aga(s(M), 0, Val) → U1_aga(M, Val, ackermann_in_aga(M, s(0), Val))
U3_aga(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s(M), s(N), Val)
U1_aga(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_aga(s(M), 0, Val)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa(x1, x3)
U1_gaa(x1, x2, x3) = U1_gaa(x3)
ackermann_in_aga(x1, x2, x3) = ackermann_in_aga(x2)
ackermann_out_aga(x1, x2, x3) = ackermann_out_aga(x1, x2, x3)
U1_aga(x1, x2, x3) = U1_aga(x3)
U2_aga(x1, x2, x3, x4) = U2_aga(x4)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x4)
U3_aga(x1, x2, x3, x4) = U3_aga(x4)
ACKERMANN_IN_GAA(x1, x2, x3) = ACKERMANN_IN_GAA(x1)
U2_AGA(x1, x2, x3, x4) = U2_AGA(x4)
ACKERMANN_IN_AGA(x1, x2, x3) = ACKERMANN_IN_AGA(x2)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_AGA(0) → ACKERMANN_IN_AGA(s)
U2_GAA(ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGA(Val1)
ACKERMANN_IN_GAA(s) → U2_GAA(ackermann_in_gaa(s))
U2_AGA(ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGA(Val1)
ACKERMANN_IN_AGA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_AGA(s) → U2_AGA(ackermann_in_gaa(s))
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_AGA(s)

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, s, Val)) → ackermann_out_gaa(s, Val)
U2_gaa(ackermann_out_gaa(s, Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, N, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s, Val)
U2_aga(ackermann_out_gaa(s, Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s, s, Val)
U1_aga(ackermann_out_aga(M, s, Val)) → ackermann_out_aga(s, 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

ACKERMANN_IN_AGA(0) → ACKERMANN_IN_AGA(s)

The remaining pairs can at least be oriented weakly.

U2_GAA(ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGA(Val1)
ACKERMANN_IN_GAA(s) → U2_GAA(ackermann_in_gaa(s))
U2_AGA(ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGA(Val1)
ACKERMANN_IN_AGA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_AGA(s) → U2_AGA(ackermann_in_gaa(s))
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_AGA(s)

Used ordering: Polynomial interpretation [25]:

POL(0) = 1
POL(ACKERMANN_IN_AGA(x₁)) = x₁
POL(ACKERMANN_IN_GAA(x₁)) = 0
POL(U1_aga(x₁)) = x₁
POL(U1_gaa(x₁)) = x₁
POL(U2_AGA(x₁)) = x₁
POL(U2_GAA(x₁)) = x₁
POL(U2_aga(x₁)) = x₁
POL(U2_gaa(x₁)) = x₁
POL(U3_aga(x₁)) = x₁
POL(U3_gaa(x₁)) = x₁
POL(ackermann_in_aga(x₁)) = 0
POL(ackermann_in_gaa(x₁)) = 0
POL(ackermann_out_aga(x₁, x₂, x₃)) = x₃
POL(ackermann_out_gaa(x₁, x₂)) = x₂
POL(s) = 0

The following usable rules [17] were oriented:

U3_gaa(ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s, Val)
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U2_aga(ackermann_out_gaa(s, Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_aga(N) → ackermann_out_aga(0, N, s)
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s, s, Val)
U2_gaa(ackermann_out_gaa(s, Val1)) → U3_gaa(ackermann_in_aga(Val1))
U1_gaa(ackermann_out_aga(M, s, Val)) → ackermann_out_gaa(s, Val)
U1_aga(ackermann_out_aga(M, s, Val)) → ackermann_out_aga(s, 0, Val)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ Narrowing

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U2_GAA(ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGA(Val1)
ACKERMANN_IN_GAA(s) → U2_GAA(ackermann_in_gaa(s))
ACKERMANN_IN_AGA(s) → ACKERMANN_IN_GAA(s)
U2_AGA(ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGA(Val1)
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_AGA(s) → U2_AGA(ackermann_in_gaa(s))
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_AGA(s)

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, s, Val)) → ackermann_out_gaa(s, Val)
U2_gaa(ackermann_out_gaa(s, Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, N, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s, Val)
U2_aga(ackermann_out_gaa(s, Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s, s, Val)
U1_aga(ackermann_out_aga(M, s, Val)) → ackermann_out_aga(s, 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule ACKERMANN_IN_GAA(s) → U2_GAA(ackermann_in_gaa(s)) at position [0] we obtained the following new rules:

ACKERMANN_IN_GAA(s) → U2_GAA(U2_gaa(ackermann_in_gaa(s)))
ACKERMANN_IN_GAA(s) → U2_GAA(U1_gaa(ackermann_in_aga(s)))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U2_GAA(ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGA(Val1)
ACKERMANN_IN_GAA(s) → U2_GAA(U2_gaa(ackermann_in_gaa(s)))
ACKERMANN_IN_GAA(s) → U2_GAA(U1_gaa(ackermann_in_aga(s)))
U2_AGA(ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGA(Val1)
ACKERMANN_IN_AGA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_AGA(s) → U2_AGA(ackermann_in_gaa(s))
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_AGA(s)

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, s, Val)) → ackermann_out_gaa(s, Val)
U2_gaa(ackermann_out_gaa(s, Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, N, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s, Val)
U2_aga(ackermann_out_gaa(s, Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s, s, Val)
U1_aga(ackermann_out_aga(M, s, Val)) → ackermann_out_aga(s, 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule ACKERMANN_IN_AGA(s) → U2_AGA(ackermann_in_gaa(s)) at position [0] we obtained the following new rules:

ACKERMANN_IN_AGA(s) → U2_AGA(U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_AGA(s) → U2_AGA(U2_gaa(ackermann_in_gaa(s)))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ ForwardInstantiation

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U2_GAA(ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGA(Val1)
ACKERMANN_IN_GAA(s) → U2_GAA(U2_gaa(ackermann_in_gaa(s)))
ACKERMANN_IN_AGA(s) → U2_AGA(U2_gaa(ackermann_in_gaa(s)))
ACKERMANN_IN_GAA(s) → U2_GAA(U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_AGA(s) → ACKERMANN_IN_GAA(s)
U2_AGA(ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGA(Val1)
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_AGA(s) → U2_AGA(U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_AGA(s)

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, s, Val)) → ackermann_out_gaa(s, Val)
U2_gaa(ackermann_out_gaa(s, Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, N, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s, Val)
U2_aga(ackermann_out_gaa(s, Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s, s, Val)
U1_aga(ackermann_out_aga(M, s, Val)) → ackermann_out_aga(s, 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
By forward instantiating [14] the rule U2_GAA(ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGA(Val1) we obtained the following new rules:

U2_GAA(ackermann_out_gaa(s, s)) → ACKERMANN_IN_AGA(s)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s) → U2_GAA(U2_gaa(ackermann_in_gaa(s)))
U2_GAA(ackermann_out_gaa(s, s)) → ACKERMANN_IN_AGA(s)
ACKERMANN_IN_GAA(s) → U2_GAA(U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_AGA(s) → U2_AGA(U2_gaa(ackermann_in_gaa(s)))
U2_AGA(ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGA(Val1)
ACKERMANN_IN_AGA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_AGA(s) → U2_AGA(U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_AGA(s)

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, s, Val)) → ackermann_out_gaa(s, Val)
U2_gaa(ackermann_out_gaa(s, Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, N, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s, Val)
U2_aga(ackermann_out_gaa(s, Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s, s, Val)
U1_aga(ackermann_out_aga(M, s, Val)) → ackermann_out_aga(s, 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
By forward instantiating [14] the rule U2_AGA(ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGA(Val1) we obtained the following new rules:

U2_AGA(ackermann_out_gaa(s, s)) → ACKERMANN_IN_AGA(s)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

                                          ↳ QDP

                                            ↳ NonTerminationProof

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s) → U2_GAA(U2_gaa(ackermann_in_gaa(s)))
ACKERMANN_IN_AGA(s) → U2_AGA(U2_gaa(ackermann_in_gaa(s)))
ACKERMANN_IN_GAA(s) → U2_GAA(U1_gaa(ackermann_in_aga(s)))
U2_GAA(ackermann_out_gaa(s, s)) → ACKERMANN_IN_AGA(s)
ACKERMANN_IN_AGA(s) → ACKERMANN_IN_GAA(s)
U2_AGA(ackermann_out_gaa(s, s)) → ACKERMANN_IN_AGA(s)
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_AGA(s) → U2_AGA(U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_AGA(s)

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, s, Val)) → ackermann_out_gaa(s, Val)
U2_gaa(ackermann_out_gaa(s, Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, N, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s, Val)
U2_aga(ackermann_out_gaa(s, Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s, s, Val)
U1_aga(ackermann_out_aga(M, s, Val)) → ackermann_out_aga(s, 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

ACKERMANN_IN_GAA(s) → U2_GAA(U2_gaa(ackermann_in_gaa(s)))
ACKERMANN_IN_AGA(s) → U2_AGA(U2_gaa(ackermann_in_gaa(s)))
ACKERMANN_IN_GAA(s) → U2_GAA(U1_gaa(ackermann_in_aga(s)))
U2_GAA(ackermann_out_gaa(s, s)) → ACKERMANN_IN_AGA(s)
ACKERMANN_IN_AGA(s) → ACKERMANN_IN_GAA(s)
U2_AGA(ackermann_out_gaa(s, s)) → ACKERMANN_IN_AGA(s)
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_GAA(s)
ACKERMANN_IN_AGA(s) → U2_AGA(U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_GAA(s) → ACKERMANN_IN_AGA(s)

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, s, Val)) → ackermann_out_gaa(s, Val)
U2_gaa(ackermann_out_gaa(s, Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, N, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s, Val)
U2_aga(ackermann_out_gaa(s, Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s, s, Val)
U1_aga(ackermann_out_aga(M, s, Val)) → ackermann_out_aga(s, 0, Val)

s = ACKERMANN_IN_GAA(s) evaluates to t =ACKERMANN_IN_GAA(s)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from ACKERMANN_IN_GAA(s) to ACKERMANN_IN_GAA(s).

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_AGG(s(M), s(N), Val) → U2_AGG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_AGG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGG(M, Val1, Val)
ACKERMANN_IN_AGG(s(M), 0, Val) → ACKERMANN_IN_AGG(M, s(0), Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(0, N, s(N)) → ackermann_out_agg(0, N, s(N))
ackermann_in_agg(s(M), 0, Val) → U1_agg(M, Val, ackermann_in_agg(M, s(0), Val))
ackermann_in_agg(s(M), s(N), Val) → U2_agg(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(0, N, s(N)) → ackermann_out_aga(0, N, s(N))
ackermann_in_aga(s(M), 0, Val) → U1_aga(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_aga(s(M), s(N), Val) → U2_aga(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_aga(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_aga(M, N, Val, ackermann_in_aga(M, Val1, Val))
U3_aga(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s(M), s(N), Val)
U1_aga(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_aga(s(M), 0, Val)
U1_gaa(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_agg(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_agg(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_agg(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_agg(s(M), s(N), Val)
U1_agg(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_agg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_agg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_agg(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_agg(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_AGG(s(M), s(N), Val) → U2_AGG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_AGG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_AGG(M, Val1, Val)
ACKERMANN_IN_AGG(s(M), 0, Val) → ACKERMANN_IN_AGG(M, s(0), Val)

The TRS R consists of the following rules:

ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_aga(M, s(0), Val))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U1_gaa(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_aga(M, Val1, Val))
ackermann_in_aga(0, N, s(N)) → ackermann_out_aga(0, N, s(N))
ackermann_in_aga(s(M), s(N), Val) → U2_aga(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U3_gaa(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_aga(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_aga(M, N, Val, ackermann_in_aga(M, Val1, Val))
ackermann_in_aga(s(M), 0, Val) → U1_aga(M, Val, ackermann_in_aga(M, s(0), Val))
U3_aga(M, N, Val, ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s(M), s(N), Val)
U1_aga(M, Val, ackermann_out_aga(M, s(0), Val)) → ackermann_out_aga(s(M), 0, Val)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa(x1, x3)
U1_gaa(x1, x2, x3) = U1_gaa(x3)
ackermann_in_aga(x1, x2, x3) = ackermann_in_aga(x2)
ackermann_out_aga(x1, x2, x3) = ackermann_out_aga(x1, x2, x3)
U1_aga(x1, x2, x3) = U1_aga(x3)
U2_aga(x1, x2, x3, x4) = U2_aga(x4)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x4)
U3_aga(x1, x2, x3, x4) = U3_aga(x4)
U2_AGG(x1, x2, x3, x4) = U2_AGG(x3, x4)
ACKERMANN_IN_AGG(x1, x2, x3) = ACKERMANN_IN_AGG(x2, x3)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_AGG(0, Val) → ACKERMANN_IN_AGG(s, Val)
U2_AGG(Val, ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGG(Val1, Val)
ACKERMANN_IN_AGG(s, Val) → U2_AGG(Val, ackermann_in_gaa(s))

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, s, Val)) → ackermann_out_gaa(s, Val)
U2_gaa(ackermann_out_gaa(s, Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, N, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s, Val)
U2_aga(ackermann_out_gaa(s, Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s, s, Val)
U1_aga(ackermann_out_aga(M, s, Val)) → ackermann_out_aga(s, 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

ACKERMANN_IN_AGG(0, Val) → ACKERMANN_IN_AGG(s, Val)

The remaining pairs can at least be oriented weakly.

U2_AGG(Val, ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGG(Val1, Val)
ACKERMANN_IN_AGG(s, Val) → U2_AGG(Val, ackermann_in_gaa(s))

Used ordering: Polynomial interpretation [25]:

POL(0) = 1
POL(ACKERMANN_IN_AGG(x₁, x₂)) = x₁
POL(U1_aga(x₁)) = x₁
POL(U1_gaa(x₁)) = x₁
POL(U2_AGG(x₁, x₂)) = x₂
POL(U2_aga(x₁)) = x₁
POL(U2_gaa(x₁)) = 0
POL(U3_aga(x₁)) = x₁
POL(U3_gaa(x₁)) = x₁
POL(ackermann_in_aga(x₁)) = 0
POL(ackermann_in_gaa(x₁)) = 0
POL(ackermann_out_aga(x₁, x₂, x₃)) = x₃
POL(ackermann_out_gaa(x₁, x₂)) = x₂
POL(s) = 0

The following usable rules [17] were oriented:

ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U2_gaa(ackermann_out_gaa(s, Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
U2_aga(ackermann_out_gaa(s, Val1)) → U3_aga(ackermann_in_aga(Val1))
U1_gaa(ackermann_out_aga(M, s, Val)) → ackermann_out_gaa(s, Val)
U3_aga(ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s, s, Val)
ackermann_in_aga(N) → ackermann_out_aga(0, N, s)
U1_aga(ackermann_out_aga(M, s, Val)) → ackermann_out_aga(s, 0, Val)
U3_gaa(ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s, Val)
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U2_AGG(Val, ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGG(Val1, Val)
ACKERMANN_IN_AGG(s, Val) → U2_AGG(Val, ackermann_in_gaa(s))

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, s, Val)) → ackermann_out_gaa(s, Val)
U2_gaa(ackermann_out_gaa(s, Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, N, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s, Val)
U2_aga(ackermann_out_gaa(s, Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s, s, Val)
U1_aga(ackermann_out_aga(M, s, Val)) → ackermann_out_aga(s, 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule ACKERMANN_IN_AGG(s, Val) → U2_AGG(Val, ackermann_in_gaa(s)) at position [1] we obtained the following new rules:

ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U2_gaa(ackermann_in_gaa(s)))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U2_gaa(ackermann_in_gaa(s)))
U2_AGG(Val, ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGG(Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, s, Val)) → ackermann_out_gaa(s, Val)
U2_gaa(ackermann_out_gaa(s, Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, N, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s, Val)
U2_aga(ackermann_out_gaa(s, Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s, s, Val)
U1_aga(ackermann_out_aga(M, s, Val)) → ackermann_out_aga(s, 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

We have to consider all (P,Q,R)-chains.
By forward instantiating [14] the rule U2_AGG(Val, ackermann_out_gaa(s, Val1)) → ACKERMANN_IN_AGG(Val1, Val) we obtained the following new rules:

U2_AGG(x0, ackermann_out_gaa(s, s)) → ACKERMANN_IN_AGG(s, x0)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ ForwardInstantiation

                                  ↳ QDP

                                    ↳ NonTerminationProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U2_gaa(ackermann_in_gaa(s)))
U2_AGG(x0, ackermann_out_gaa(s, s)) → ACKERMANN_IN_AGG(s, x0)

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, s, Val)) → ackermann_out_gaa(s, Val)
U2_gaa(ackermann_out_gaa(s, Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, N, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s, Val)
U2_aga(ackermann_out_gaa(s, Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s, s, Val)
U1_aga(ackermann_out_aga(M, s, Val)) → ackermann_out_aga(s, 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0)
ackermann_in_aga(x0)
U3_gaa(x0)
U2_aga(x0)
U3_aga(x0)
U1_aga(x0)

ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U1_gaa(ackermann_in_aga(s)))
ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U2_gaa(ackermann_in_gaa(s)))
U2_AGG(x0, ackermann_out_gaa(s, s)) → ACKERMANN_IN_AGG(s, x0)

The TRS R consists of the following rules:

ackermann_in_gaa(s) → U1_gaa(ackermann_in_aga(s))
ackermann_in_gaa(s) → U2_gaa(ackermann_in_gaa(s))
U1_gaa(ackermann_out_aga(M, s, Val)) → ackermann_out_gaa(s, Val)
U2_gaa(ackermann_out_gaa(s, Val1)) → U3_gaa(ackermann_in_aga(Val1))
ackermann_in_aga(N) → ackermann_out_aga(0, N, s)
ackermann_in_aga(s) → U2_aga(ackermann_in_gaa(s))
U3_gaa(ackermann_out_aga(M, Val1, Val)) → ackermann_out_gaa(s, Val)
U2_aga(ackermann_out_gaa(s, Val1)) → U3_aga(ackermann_in_aga(Val1))
ackermann_in_aga(0) → U1_aga(ackermann_in_aga(s))
U3_aga(ackermann_out_aga(M, Val1, Val)) → ackermann_out_aga(s, s, Val)
U1_aga(ackermann_out_aga(M, s, Val)) → ackermann_out_aga(s, 0, Val)

s = U2_AGG(x0, U1_gaa(ackermann_in_aga(s))) evaluates to t =U2_AGG(x0, U1_gaa(ackermann_in_aga(s)))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

U2_AGG(x0, U1_gaa(ackermann_in_aga(s))) → U2_AGG(x0, U1_gaa(ackermann_out_aga(0, s, s)))
with rule ackermann_in_aga(N) → ackermann_out_aga(0, N, s) at position [1,0] and matcher [N / s]

U2_AGG(x0, U1_gaa(ackermann_out_aga(0, s, s))) → U2_AGG(x0, ackermann_out_gaa(s, s))
with rule U1_gaa(ackermann_out_aga(M, s, Val)) → ackermann_out_gaa(s, Val) at position [1] and matcher [M / 0, Val / s]

U2_AGG(x0, ackermann_out_gaa(s, s)) → ACKERMANN_IN_AGG(s, x0)
with rule U2_AGG(x0', ackermann_out_gaa(s, s)) → ACKERMANN_IN_AGG(s, x0') at position [] and matcher [x0' / x0]

ACKERMANN_IN_AGG(s, x0) → U2_AGG(x0, U1_gaa(ackermann_in_aga(s)))
with rule ACKERMANN_IN_AGG(s, y0) → U2_AGG(y0, U1_gaa(ackermann_in_aga(s)))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.